This disclosure teaches novel techniques related to image computation. Specifically, techniques for decision heuristics for image computation using boolean satisfiability tests (SATs) and binary decision diagrams (BDDs) that are based on partitions are taught. The disclosed teachings are embodied in methods for image computation.
1. References
The following papers provide useful background information, for which they are incorporated herein by reference in their entirety, and are selectively referred to in the remainder of this disclosure by their accompanying reference numbers in square brackets (i.e., [3] for the third numbered paper by A Biere et al.):
[1] P. A. Abdulla, P. Bjesse, and N. Een. Symbolic reachability analysis based on SAT-solvers. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 2000.
[2] E. Amir and S. McIlraith. Partition-based logical reasoning. In Proc. 7th International Conference on Principles of Knowledge Representation and Reasoning, 2000.
[3] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without BDDS. In Tools and Algorithms for the Analysis and Construction of Systems (TACAS), volume 1579 of LNCS, 1999.
[4] R. K. Brayton et al. VIS: A system for verification and synthesis. In R. Alur and T. Henzinger, editors, Proc. mt. Conf. on Comput.-Aided Verification, volume 1102 of LNCS, pages 428-432, June 1996.
[5] R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Tran. on Comp., C-35(8):677-691, August 1986.
[6] J. Burch and V. Singhal. Tight integration of combinational verification methods. In Proc. Int. Conf. on Comput.-Aided Design, pages 570-576, 1998.
[7] J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Tran. on CAD of Integrated Circ. and Sys., 13(4):401-424, Aprial 1994.
[8] G. Cabodi, P. Camurati, and S. Quer. Biasing symbolic search by means of dynamic activity profiles. In Proc. Conference on Design Automation and Test Europe (DATE), March 2001.
[9] P. Chauhan, E. M. Clarke, S. Jha, J. Kukula, T. Shiple, H. Veith, and D. Wang. Non-linear quantification scheduling in image computation. In Proc. Int. Conf. on Comput.-Aided Design, November 2001.
[10] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
[11] O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines using symbolic execution. In Proc. Int. Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 365-373. Springer-Verlag, June 1989.
[12] A. Gupta and P. Ashar. Integrating a Boolean satisfiability checker and BDDs for combinational verification. In Proc. VLSI Design Conference, January 1998.
[13] A. Gupta, Z. Yang, A. Gupta, and P. Ashar. SAT-based image computation with application in reachability analysis. In Proc. Conference on Formal Methods in Computer-Aided Design, November 2000.
[14] G. Karypis et al. hMETIS: Serial hypergraph and circuit partitioning.
http://www-users.cs.umn.edu/xcx9ckarypis/metis/hmetis.
[15] J. Kukula. When is SAT hard? Presented at Dagstuhl Seminar Design and Test on BDDs versus SAT, Schloss Dagstuhl, Germany, January 2001.
[16] T. Lengauer. Combinatorial Algorithms for Integrated Circuit Layout. John Wiley and Sons, England, 1990.
[17] J. P. Marques-Silva. Search Algorithms for Satisfiability Problems in Combinational Switching Circuits. PhD thesis, EEOS Department, University of Michigan, May 1995.
[18] J. P. Marques-Silva and A. L. Oliveira. Improving satisfiability algorithms with dominance and partitioning. In IEEE/ACM International Workshop on Logic Synthesis, May 1997.
[19] J. P. Marquez-Silva. Grasp package.
http://algos.inesc.pt/xcx9cjpms/software.html.
[20] I.-H. Moon, G. Haclitel, and F. Somenzi. Border-block triangular form and conjunction schedule in image computation. In Proc. Conference on Formal Methods in Computer-Aided Design, November 2000.
[21] I.-H. Moon, J. Kukula, K. Ravi, and F. Somenzi. To split or to conjoin: The question in image computation. In Proc. Design Automation Conf., pages 23-28, June 2000.
[22] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. Design Automation Conf., June 2001.
[23] V. Paruthi and A. Kuehlmann. Equivalence checking combining a structural SAT-Solver, BDDs and simulation. In Proc. Int. Conf on Comput. Design, October 2000.
[24] M. R. Prasad, P. Chong, and K. Keutzer. Why is ATPG easy? In Proc. Design Automation Conf., pages 22-28, 1999.
[25] R. K. Ranjan, A. Aziz, R. K. Brayton, B. F. Plessier, and C. Pixley. Efficient BDD algorithms for FSM synthesis and verification. In International Workshop for Logic Synthesis, May 1995. Lake Tahoe, Calif.
[26] M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a SAT-Solver. In Proc. Conference on Formal Methods in Computer-Aided Design, November 2000.
[27] F. Somenzi et al. CUDD: University of Colorado Decision Diagram Package.
mhttp://visi.colorado.eduefabio/CUDD/.
[28] H. Zhang. SATO: an efficient propositional prover. In International Conference on Automated Deduction, number 1249 in LNAI, pages 272-275, 1997.
2. Related Work
The Boolean satisfiability problem (SAT) has conventionally been used in many verification applications, such as equivalence checking [6, 12, 23], as well as model checking [1, 3, 26]. Combining SAT techniques with BDDs has also been conventionally shown to be effective for image computation with application in state reachability analysis of sequential circuits [13].
A typical implementation for solving SAT uses a branch-and-bound search over the values of all variables, with considerable sophistication in the software engineering of techniques for decision making, implication gathering, and back-tracking [19, 22, 28]. Since the SAT problem itself is NP-complete, the effectiveness of any algorithm for solving SAT depends upon the amount of pruning of the search space enabled by the SAT. In solving the SAT problem, decision heuristics are used to decide on the choice of which SAT variable to branch on at a given point in the solution. Such decision heuristics and their values, directly affect the amount of pruning.
Many SAT implementations use a Conjunctive Normal Form (CNF) representation of the Boolean formula associated with the SAT. This has led to the development of many decision heuristics based on the frequency of appearance of variables in unsatisfied (or all) clauses. In these decision heuristics, sometimes preference is given to smaller clauses in order to facilitate implications [17].
The present disclosure focuses on decision heuristics targeted at decomposing the overall problem into smaller, unrelated, partitions.
There have been some efforts in exploring the benefits of partitioning for generic SAT applications in CAD [18]. But, such efforts were restricted to the detection of partitions as they arise dynamically within the search, and no effort was made to actually derive such partitions. There has been some recent independent work on use of partitioning methods, including the use of separator-based partitioning, to improve the efficiency of the SAT solver [2]. However, this effort is not directly targeted at deriving good decision heuristics. In that work [2], the SAT problem is recursively partitioned into a tree of SAT subproblems using vertex separators as we do, but the manner in which they use the separators is completely different. Rather than deriving good decision heuristics based on the partitions, they find all solutions of each subproblem independently. Once all such solutions are found, they attempt to determine if any combination of solutions from each subproblem is consistent in terms of the values on the variables shared between subproblems. This is extremely inefficient when large SAT problems are being solved.
Along another related line, it has been conjectured that the degree of difficulty of a given SAT problem is related to the xe2x80x9cinformation bandwidthxe2x80x9d of the problem [15, 24]. That is, the greater the connectivity between variables, the more difficult is the problem likely to be. Again, this observation can be used to justify choosingdecision variables that partition the problem into low bandwidth (or disjoint) partitions.
In terms of image computation itself, there have been many efforts aimed at exploiting circuit structure information for a pure BDD-based image computation [10]. For example, heuristics for clustering and ordering are based on analysis of shared variable support sets between next-state bit relations and the input state set [25]. In particular, Moon et al. proposed the MLP algorithm for a dependency matrix representation to obtain a Bordered Block Triangular form, which is particularly suited for deriving a good conjunction schedule [20]. They also identify existing connected components for decomposition, but again, there is no effort to actively derive such decompositions. Note that many of these heuristics capture the benefits of partitioning on the underlying circuit structure. However, none of these methods use SAT.
3. SAT-based Image Computation
Some background information on Image computation based on SAT is provided herein. Historically, symbolic state space traversal [7, 11] has relied on efficient algorithms based on BDDs [5] for carrying out an image computation, shown below:
Image(Y)=∃X,WT(X,W,Y){circumflex over ( )}From(X)xe2x80x83xe2x80x83(1)
Here, X/Y denote present/next state variables, respectively, W denotes primary input variables, T denotes the transition relation, and From denotes the input state set. BDDs are used to represent the characteristic function of the transition relation, as well as the input/image sets. As an example application, the set of reachable states can be computed by starting with a set From which denotes the set of initial states of a system, and using image computation iteratively, until a fixpoint is reached. The BDD-based approaches work well when it is possible to represent the sets of states and the transition relation (as a whole, or in a usefully partitioned form) using BDDs. Unfortunately, BDD size is very sensitive to the number of variables, variable ordering, and the nature of the logic expressions being represented.
Recently, an integration of SAT and BDDs has been proposed for image computation [13]. A pictorial representation of various features of this method is shown in FIG. 1. As shown in Part (a), state sets are represented by BDDs, and the transition relation is represented as a CNF formula. All image solutions over Y are enumerated using a backtracking search algorithm for SAT which operates over the CNF formula for T. Within this search, the BDD for From(X) is used as a constraint (called BDD Bounding), where any partial assignment over the X variables that does not satisfy From(X) leads to immediate backtracking within SAT.
As shown in Part (b), rather than using SAT to enumerate each solution all the way down to a leaf, BDD-based subproblems are invoked at intermediate points within the SAT search. This allows a symbolic, rather than explicit, enumeration of all solutions in the subtree rooted below that point. In a sense, this approach can be regarded as SAT providing a disjunctive decomposition of the image computation into many BDD subproblems. Each of the BDD subproblems involves a standard image computation as shown in Part (c), where the BDDs for the conjunctive partition are generated on-the-fly from unsatisfied clauses of the CNF for T.
A conventional method for image computation uses SAT search as a disjunctive decomposition of the overall search for image solutions into multiple subproblems, each of which is handled by using a standard BDD-based image computation algorithm [13]. In this context, SAT decision heuristics affect not only the pruning of the search space in SAT, but also the complexity of dynamically generated BDD subproblems.
The benefits of complementing a purely functional approach based on BDDs with structural information captured by SAT is crucial in improving performance of image computation. It will be advantageous to develop heuristics that improves the performance of reachability analysis, as well as helping in reaching more states than possible otherwise.
The disclosed teachings are aimed at realizing some of the advantages noted above. According to an aspect of the disclosed techniques, there is provided a method for Boolean Satisfiability (SAT). The method comprising using a variable decision heuristic in a SAT algorithm; and pruning the search space of SAT using said decision heuristic. The decision heuristic is based on partitioning a conjunctive normal form (CNF) of a Boolean formula corresponding to the SAT and the partitioning is induced by a separator set.
Another aspect of the disclosed techniques is a method of image computation, wherein said image computation uses Boolean Satisfiability (SAT) and binary decision diagrams (BDD). The SAT is performed by a process comprising using a variable decision heuristic in a SAT algorithm; and pruning the search space of SAT using said decision heuristic. The decision heuristic is based on partitioning a conjunctive normal form (CNF) of a Boolean formula corresponding to the SAT and said partitioning is induced by a separator set.
In a specific improvement the decision heuristic is targeted at variables that dynamically result in partitioning a problem corresponding to the SAT into subproblems consisting of clauses with disjoint variable support.
In another specific improvement the partitioning is performed recursively on existing partitions whose sizes are above a threshold.
In still another specific improvement during the SAT preference is given to making decisions on separator variables.
In yet another specific improvement the partitioning is done using a dependency matrix.
More specifically, the rows of the dependency matrix contain conjunctive partitions and columns of the dependency matrix contains variable corresponding to said conjunctive partitions.
More specifically, a minimum number of clauses are considered for each gate such that all dependencies are captured.
More specifically, an additional row is added to the dependency matrix to denote dependency of an input set corresponding to the BDD to various variables.
More specifically, a column is selected from an active region of the matrix that intersects a maximum number of shortest rows, said column is moved to leftmost position and the active region is shrunk to exclude the selected column.
Still more specifically, rules are incorporated to break ties whenever there are multiple columns that can be moved to the left.
Even more specifically, the rule comprises giving preference to columns with a most number of entries in an inactive region.
In another specific improvement, the partitioning is done using a hypergraph partitioning technique.
More specifically, a CNF graph is used, where nodes denote clauses and hyperedges denote variables of formulae corresponding to the CNF.
More specifically, a node is added to the CNF graph to represent inputs of the BDD.
Still more specifically, each hyperedge is provided a weight that is equal to a number of nodes said each hyperedge connects to.
More specifically, a minimum-weight cutset of the graph is determined such that the cutset partitions the graph into unconnected components.
Still more specifically, the minimum weight cutset comprises hyperedges.
Still more specifically, a separator partition is defined as all clause that variables corresponding to hyperedges in the minimum weight cutset appear in.
In another specific improvement, wherein the partitioning results in a partition tree such that a size of each terminal partition is less than a threshold.
More specifically, the partition tree is used to assign a weight each to each variable in the CNF representation.
Still more specifically, the weight is used to rank variables.
More specifically, terminals corresponding to the separator are assigned a weight of 2 and other terminals are assigned a weight of 1.
More specifically, shared separator variables are give more preference that private separator variables.
Still more specifically, the preference is implemented by calculating a weight for a variable by adding contributions from each terminal partition that the variable appears in.
More specifically, the weight assigned to each terminal partition decreased according to increased depth from top of the partition tree.
More specifically, smaller partitions are given higher weight.